Termination w.r.t. Q proof of /tmp/tmpCbeCSz/maxsortcondition.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

Q is empty.

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
MAX(cons(x, cons(y, xs))) → GE(x, y)
IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
DEL(x, cons(y, xs)) → EQ(x, y)
IF2(false, x, y, xs) → DEL(x, xs)
EQ(s(x), s(y)) → EQ(x, y)
SORT(xs) → IF3(empty(xs), xs)
SORT(xs) → EMPTY(xs)
IF3(false, xs) → SORT(del(max(xs), xs))
IF3(false, xs) → DEL(max(xs), xs)
IF3(false, xs) → MAX(xs)
GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
MAX(cons(x, cons(y, xs))) → GE(x, y)
IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
DEL(x, cons(y, xs)) → EQ(x, y)
IF2(false, x, y, xs) → DEL(x, xs)
EQ(s(x), s(y)) → EQ(x, y)
SORT(xs) → IF3(empty(xs), xs)
SORT(xs) → EMPTY(xs)
IF3(false, xs) → SORT(del(max(xs), xs))
IF3(false, xs) → DEL(max(xs), xs)
IF3(false, xs) → MAX(xs)
GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 5 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

R is empty.
The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

GE(s(x), s(y)) → GE(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

R is empty.
The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x), s(y)) → EQ(x, y)

From the DPs we obtained the following set of size-change graphs:

EQ(s(x), s(y)) → EQ(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x, y, xs) → DEL(x, xs)
DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

DEL(x, cons(y, xs)) → IF2(eq(x, y), x, y, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF2(false, x, y, xs) → DEL(x, xs)
The graph contains the following edges 2 >= 1, 4 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPOrderProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x, y, xs) → MAX(cons(x, xs))
MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)
IF1(false, x, y, xs) → MAX(cons(y, xs))

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MAX(cons(x, cons(y, xs))) → IF1(ge(x, y), x, y, xs)

The remaining pairs can at least be oriented weakly.

IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(IF1(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(MAX(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₂
POL(false) = 0
POL(ge(x₁, x₂)) = 0
POL(s(x₁)) = 0
POL(true) = 0

The following usable rules [FROCOS05] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x, y, xs) → MAX(cons(x, xs))
IF1(false, x, y, xs) → MAX(cons(y, xs))

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF3(false, xs) → SORT(del(max(xs), xs))
SORT(xs) → IF3(empty(xs), xs)

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
sort(xs) → if3(empty(xs), xs)
if3(true, xs) → nil
if3(false, xs) → sort(del(max(xs), xs))
empty(nil) → true
empty(cons(x, xs)) → false
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF3(false, xs) → SORT(del(max(xs), xs))
SORT(xs) → IF3(empty(xs), xs)

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, xs)) → false
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
sort(x0)
if3(true, x0)
if3(false, x0)
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

sort(x0)
if3(true, x0)
if3(false, x0)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

IF3(false, xs) → SORT(del(max(xs), xs))
SORT(xs) → IF3(empty(xs), xs)

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, xs)) → false
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule SORT(xs) → IF3(empty(xs), xs) at position [0] we obtained the following new rules [LPAR04]:

SORT(nil) → IF3(true, nil)
SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

IF3(false, xs) → SORT(del(max(xs), xs))
SORT(nil) → IF3(true, nil)
SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, xs)) → false
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
IF3(false, xs) → SORT(del(max(xs), xs))

The TRS R consists of the following rules:

empty(nil) → true
empty(cons(x, xs)) → false
max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
IF3(false, xs) → SORT(del(max(xs), xs))

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
empty(nil)
empty(cons(x0, x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

empty(nil)
empty(cons(x0, x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
IF3(false, xs) → SORT(del(max(xs), xs))

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By instantiating [LPAR04] the rule IF3(false, xs) → SORT(del(max(xs), xs)) we obtained the following new rules [LPAR04]:

IF3(false, cons(z0, z1)) → SORT(del(max(cons(z0, z1)), cons(z0, z1)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))
IF3(false, cons(z0, z1)) → SORT(del(max(cons(z0, z1)), cons(z0, z1)))

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

This DP could be deleted by the Induction-Processor:
IF3(false, cons(z0', z1')) → SORT(del(max(cons(z0', z1')), cons(z0', z1')))

This order was computed:
Polynomial interpretation [POLO]:

POL(0) = 0
POL(IF3(x₁, x₂)) = x₂
POL(SORT(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(del(x₁, x₂)) = x₂
POL(eq(x₁, x₂)) = x₂
POL(false) = 0
POL(ge(x₁, x₂)) = 0
POL(if1(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄
POL(if2(x₁, x₂, x₃, x₄)) = 1 + x₃ + x₄
POL(max(x₁)) = x₁
POL(nil) = 0
POL(s(x₁)) = x₁
POL(true) = 0

At least one of these decreasing rules is always used after the deleted DP:
if2(true, x1499, y1039, xs689) → xs689

The following formula is valid:
z0:sort[a34].(¬(z0 =nil)→del'(max(z0 ), z0 )=true)

The transformed set:
del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                  ↳ DependencyGraphProof

                                                ↳ QTRS

Q DP problem:
The TRS P consists of the following rules:

SORT(cons(x0, x1)) → IF3(false, cons(x0, x1))

The TRS R consists of the following rules:

max(nil) → 0
max(cons(x, nil)) → x
max(cons(x, cons(y, xs))) → if1(ge(x, y), x, y, xs)
if1(true, x, y, xs) → max(cons(x, xs))
if1(false, x, y, xs) → max(cons(y, xs))
del(x, nil) → nil
del(x, cons(y, xs)) → if2(eq(x, y), x, y, xs)
eq(0, 0) → true
eq(0, s(y)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
if2(true, x, y, xs) → xs
if2(false, x, y, xs) → cons(y, del(x, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

Q is empty.

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

DEL'(x81, cons(y55, xs37)) → IF2'(eq(x81, y55), x81, y55, xs37)
DEL'(x81, cons(y55, xs37)) → EQ(x81, y55)
IF2'(false, x163, y113, xs75) → DEL'(x163, xs75)
MAX(cons(x25, cons(y16, xs10))) → IF1(ge(x25, y16), x25, y16, xs10)
MAX(cons(x25, cons(y16, xs10))) → GE(x25, y16)
IF1(true, x39, y26, xs17) → MAX(cons(x39, xs17))
IF1(false, x53, y36, xs24) → MAX(cons(y36, xs24))
DEL(x81, cons(y55, xs37)) → IF2(eq(x81, y55), x81, y55, xs37)
DEL(x81, cons(y55, xs37)) → EQ(x81, y55)
EQ(s(x135), s(y93)) → EQ(x135, y93)
IF2(false, x163, y113, xs75) → DEL(x163, xs75)
GE(s(x205), s(y141)) → GE(x205, y141)
EQUAL_SORT[A33](s(x0), s(x1)) → EQUAL_SORT[A33](x0, x1)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)

The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

DEL'(x81, cons(y55, xs37)) → IF2'(eq(x81, y55), x81, y55, xs37)
DEL'(x81, cons(y55, xs37)) → EQ(x81, y55)
IF2'(false, x163, y113, xs75) → DEL'(x163, xs75)
MAX(cons(x25, cons(y16, xs10))) → IF1(ge(x25, y16), x25, y16, xs10)
MAX(cons(x25, cons(y16, xs10))) → GE(x25, y16)
IF1(true, x39, y26, xs17) → MAX(cons(x39, xs17))
IF1(false, x53, y36, xs24) → MAX(cons(y36, xs24))
DEL(x81, cons(y55, xs37)) → IF2(eq(x81, y55), x81, y55, xs37)
DEL(x81, cons(y55, xs37)) → EQ(x81, y55)
EQ(s(x135), s(y93)) → EQ(x135, y93)
IF2(false, x163, y113, xs75) → DEL(x163, xs75)
GE(s(x205), s(y141)) → GE(x205, y141)
EQUAL_SORT[A33](s(x0), s(x1)) → EQUAL_SORT[A33](x0, x1)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → AND(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)

The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 7 SCCs with 4 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)

The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)

R is empty.
The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ QDPSizeChangeProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)

From the DPs we obtained the following set of size-change graphs:

EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x1, x3)
The graph contains the following edges 1 > 1, 2 > 2
EQUAL_SORT[A34](cons(x0, x1), cons(x2, x3)) → EQUAL_SORT[A34](x0, x2)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A33](s(x0), s(x1)) → EQUAL_SORT[A33](x0, x1)

The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A33](s(x0), s(x1)) → EQUAL_SORT[A33](x0, x1)

R is empty.
The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ QDPSizeChangeProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQUAL_SORT[A33](s(x0), s(x1)) → EQUAL_SORT[A33](x0, x1)

From the DPs we obtained the following set of size-change graphs:

EQUAL_SORT[A33](s(x0), s(x1)) → EQUAL_SORT[A33](x0, x1)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x205), s(y141)) → GE(x205, y141)

The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x205), s(y141)) → GE(x205, y141)

R is empty.
The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ QDPSizeChangeProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x205), s(y141)) → GE(x205, y141)

From the DPs we obtained the following set of size-change graphs:

GE(s(x205), s(y141)) → GE(x205, y141)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x135), s(y93)) → EQ(x135, y93)

The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x135), s(y93)) → EQ(x135, y93)

R is empty.
The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ QDPSizeChangeProof

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(x135), s(y93)) → EQ(x135, y93)

From the DPs we obtained the following set of size-change graphs:

EQ(s(x135), s(y93)) → EQ(x135, y93)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x163, y113, xs75) → DEL(x163, xs75)
DEL(x81, cons(y55, xs37)) → IF2(eq(x81, y55), x81, y55, xs37)

The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x163, y113, xs75) → DEL(x163, xs75)
DEL(x81, cons(y55, xs37)) → IF2(eq(x81, y55), x81, y55, xs37)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ QDPSizeChangeProof

                                                              ↳ QDP

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(false, x163, y113, xs75) → DEL(x163, xs75)
DEL(x81, cons(y55, xs37)) → IF2(eq(x81, y55), x81, y55, xs37)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))

From the DPs we obtained the following set of size-change graphs:

DEL(x81, cons(y55, xs37)) → IF2(eq(x81, y55), x81, y55, xs37)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF2(false, x163, y113, xs75) → DEL(x163, xs75)
The graph contains the following edges 2 >= 1, 4 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x39, y26, xs17) → MAX(cons(x39, xs17))
MAX(cons(x25, cons(y16, xs10))) → IF1(ge(x25, y16), x25, y16, xs10)
IF1(false, x53, y36, xs24) → MAX(cons(y36, xs24))

The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x39, y26, xs17) → MAX(cons(x39, xs17))
MAX(cons(x25, cons(y16, xs10))) → IF1(ge(x25, y16), x25, y16, xs10)
IF1(false, x53, y36, xs24) → MAX(cons(y36, xs24))

The TRS R consists of the following rules:

ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ QDPOrderProof

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x39, y26, xs17) → MAX(cons(x39, xs17))
MAX(cons(x25, cons(y16, xs10))) → IF1(ge(x25, y16), x25, y16, xs10)
IF1(false, x53, y36, xs24) → MAX(cons(y36, xs24))

The TRS R consists of the following rules:

ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MAX(cons(x25, cons(y16, xs10))) → IF1(ge(x25, y16), x25, y16, xs10)

The remaining pairs can at least be oriented weakly.

IF1(true, x39, y26, xs17) → MAX(cons(x39, xs17))
IF1(false, x53, y36, xs24) → MAX(cons(y36, xs24))

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(IF1(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(MAX(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₂
POL(false) = 0
POL(ge(x₁, x₂)) = 0
POL(s(x₁)) = 0
POL(true) = 0

The following usable rules [FROCOS05] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ QDPOrderProof

                                                                          ↳ QDP

                                                                            ↳ DependencyGraphProof

                                                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, x39, y26, xs17) → MAX(cons(x39, xs17))
IF1(false, x53, y36, xs24) → MAX(cons(y36, xs24))

The TRS R consists of the following rules:

ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

IF2'(false, x163, y113, xs75) → DEL'(x163, xs75)
DEL'(x81, cons(y55, xs37)) → IF2'(eq(x81, y55), x81, y55, xs37)

The TRS R consists of the following rules:

del'(x67, nil) → false
del'(x81, cons(y55, xs37)) → if2'(eq(x81, y55), x81, y55, xs37)
if2'(true, x149, y103, xs68) → true
if2'(false, x163, y113, xs75) → del'(x163, xs75)
max(nil) → 0
max(cons(x11, nil)) → x11
max(cons(x25, cons(y16, xs10))) → if1(ge(x25, y16), x25, y16, xs10)
if1(true, x39, y26, xs17) → max(cons(x39, xs17))
if1(false, x53, y36, xs24) → max(cons(y36, xs24))
del(x67, nil) → nil
del(x81, cons(y55, xs37)) → if2(eq(x81, y55), x81, y55, xs37)
eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)
if2(true, x149, y103, xs68) → xs68
if2(false, x163, y113, xs75) → cons(y113, del(x163, xs75))
ge(x177, 0) → true
ge(0, s(x191)) → false
ge(s(x205), s(y141)) → ge(x205, y141)
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a33](0, 0) → true
equal_sort[a33](0, s(x0)) → false
equal_sort[a33](s(x0), 0) → false
equal_sort[a33](s(x0), s(x1)) → equal_sort[a33](x0, x1)
equal_sort[a34](nil, nil) → true
equal_sort[a34](nil, cons(x0, x1)) → false
equal_sort[a34](cons(x0, x1), nil) → false
equal_sort[a34](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a34](x0, x2), equal_sort[a34](x1, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63]) → true

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

IF2'(false, x163, y113, xs75) → DEL'(x163, xs75)
DEL'(x81, cons(y55, xs37)) → IF2'(eq(x81, y55), x81, y55, xs37)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)

The set Q consists of the following terms:

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del'(x0, nil)
del'(x0, cons(x1, x2))
if2'(true, x0, x1, x2)
if2'(false, x0, x1, x2)
max(nil)
max(cons(x0, nil))
max(cons(x0, cons(x1, x2)))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
del(x0, nil)
del(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
equal_bool(true, false)
equal_bool(false, true)
equal_bool(true, true)
equal_bool(false, false)
and(true, x0)
and(false, x0)
or(true, x0)
or(false, x0)
not(false)
not(true)
isa_true(true)
isa_true(false)
isa_false(true)
isa_false(false)
equal_sort[a33](0, 0)
equal_sort[a33](0, s(x0))
equal_sort[a33](s(x0), 0)
equal_sort[a33](s(x0), s(x1))
equal_sort[a34](nil, nil)
equal_sort[a34](nil, cons(x0, x1))
equal_sort[a34](cons(x0, x1), nil)
equal_sort[a34](cons(x0, x1), cons(x2, x3))
equal_sort[a63](witness_sort[a63], witness_sort[a63])

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Narrowing

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ QDP

                                ↳ UsableRulesProof

                                  ↳ QDP

                                    ↳ QReductionProof

                                      ↳ QDP

                                        ↳ Instantiation

                                          ↳ QDP

                                            ↳ Induction-Processor

                                              ↳ AND

                                                ↳ QDP

                                                ↳ QTRS

                                                  ↳ Overlay + Local Confluence

                                                    ↳ QTRS

                                                      ↳ DependencyPairsProof

                                                        ↳ QDP

                                                          ↳ DependencyGraphProof

                                                            ↳ AND

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                              ↳ QDP

                                                                ↳ UsableRulesProof

                                                                  ↳ QDP

                                                                    ↳ QReductionProof

                                                                      ↳ QDP

                                                                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

IF2'(false, x163, y113, xs75) → DEL'(x163, xs75)
DEL'(x81, cons(y55, xs37)) → IF2'(eq(x81, y55), x81, y55, xs37)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(y74)) → false
eq(s(x121), 0) → false
eq(s(x135), s(y93)) → eq(x135, y93)

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))

From the DPs we obtained the following set of size-change graphs:

DEL'(x81, cons(y55, xs37)) → IF2'(eq(x81, y55), x81, y55, xs37)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF2'(false, x163, y113, xs75) → DEL'(x163, xs75)
The graph contains the following edges 2 >= 1, 4 >= 2